\aux{dniCheckIn}{c: CheckIn}{DNI}{prm(c)} 

\vspace{0.2cm}

\aux{dniCheckOut}{c: CheckOut}{DNI}{prm(c)}

\vspace{0.2cm}

\aux{fechaCheckIn}{c: CheckIn}{Fecha}{snd(c)}

\vspace{0.2cm}

\aux{fechaCheckOut}{c: CheckOut}{Fecha}{snd(c)}

\vspace{0.2cm}

\aux{ingresosDe}{h: Hotel, d: DNI}{[CheckIn]}{[ x | x \selec ingresos(h), dniCheckIn(prm(x))==d]}

\vspace{0.2cm}

\aux{salidasDe}{h: Hotel, d: DNI}{[CheckOut]}{[ x | x \selec salidas(h), dniCheckOut(prm(x))==d]}

\vspace{0.2cm}

%\aux{existeUnIngresoSinSalida}{h: Hotel, o1: CheckOut}{\bool}{\\ 
%(\exists i \selec ingresosDe(h, dniCheckOut(o1)), fechaCheckIn(i) < fechaCheckOut(o1))\\ \ 
%\neg (\exists o2 \selec salidasDe(h, dniCheckOut(o1)), fechaCheckIn(i) < fechaCheckOut(o2) < %fechaCheckOut(o1)}
%
%\vspace{0.2cm}

%\aux{existeUnIngresoElMismoDia}{h: Hotel, d: DNI, f: Fecha}{\bool}{\\
%(\exists i \selec ingresosDe(h, d)) fechaCheckIn(i) ==  f }
%
%\vspace{0.2cm}

\aux{existeUnaHabitacionDelTipo}{h: Hotel, t: TipoHabitacion}{\bool}{(\exists x \selec habitaciones(h)) tipo(x)==t}

\vspace{0.2cm}

\aux{capacidad}{h: Hotel}{\ent}{\comp{cantidadHuespedes(tipo(h))}{h \selec habitaciones(h)}}

\vspace{0.2cm}

\aux{cantidadHuespedes}{t: TipoHabitacion}{\ent}{\\ \IfThenElse{t==Simple}{1}{(\IfThenElse{t==Doble}{2}{(\IfThenElse{t==Triple}{3}{4})})}}

\vspace{0.2cm}

%\aux{compartenCadena}{hss: [[Hotel]]}{\bool}{(\forall hs \selec hss) sonDeLaMismaCadena(hs)}
%
%\vspace{0.2cm}

%\aux{sonDeLaMismaCadena}{hs: [Hotel]}{\bool}{(\forall h1,h2 \selec hs) cadena(h1)==cadena(h2)}
%
%\vspace{0.2cm}

%\aux{todosLosHoteles}{m: MinisterioDeTurismo}{[Hotel]}{\comp{h}{p \selec secretarias(m), h \selec %registro(m,p)}}
%
%\vspace{0.2cm}

%\aux{todosLosNombres}{hs: [Hotel]}{String]}{\comp{nombre(h)}{h \selec hs}}
%
%\vspace{0.2cm}

\aux{aplanar}{xss: [[T]]}{[T]}{\comp{x}{xs \selec xss, x \selec xs}}

\vspace{0.2cm}

\aux{ordenada}{l:[T]}{\bool}{(\forall i \selec [0.. \longitud{l}-1)) l_i \leq l_{i+1}}

\vspace{0.2cm}

\aux{sinRepetidos}{l: [T]}{\bool}{(\forall i, j \selec [0.. \longitud{l}), i \neq j) l_i \neq l_j}

\vspace{0.2cm}

\aux{sacarRepetidos}{l: [T]}{\bool}{(\forall i \selec [0.. \longitud{l})) l_i \notin l_[i+1..longitud(l)-1)}







